(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)


include "arithmetics/nat.ma".
include "basics/bool.ma".
include "basics/lists/list.ma".
include "basics/logic.ma".

                                                  (*        *
                                                   *  Types *
                                                   *        *)
                                                   
inductive lit : Type[0] ≝
  int : bool → nat → lit. 
  
inductive operator : Type[0] ≝
  par : operator
| copar : operator
| seq : operator.  

inductive struct : Type[0] ≝
|  unit : struct
|  atom : lit → struct
|  lista : operator → list struct → struct.



                                                  (*            *
                                                   *  Notations *
                                                   *            *)
                                                   
notation "+x" with precedence 80 for @{int true $x}.
notation "-x" with precedence 80 for @{int false $x}.
notation "∘" with precedence 80 for @{(unit))}.
(*Qui sarebbe bello poter usare i caratteri*)
notation "x+" with precedence 100 for @{((atom +($x)))}.  
notation "x^" with precedence 100 for @{((atom -($x)))}.

notation "〚 list0 x sep ; 〛" (*qui ci vorrebbe , *)
  non associative with precedence 90
  for @{(*create_struct *)(lista par ${fold right @'nil rec acc @{'cons $x $acc}})}.


notation "❨ list0 x sep ; ❩"  (*qui ci vorrebbe , *)
  non associative with precedence 90
  for @{(*create_struct *)(lista copar ${fold right @'nil rec acc @{'cons $x $acc}})}.
  
notation "❮ list0 x sep ; ❯"
  non associative with precedence 90
  for @{(*create_struct*) (lista seq ${fold right @'nil rec acc @{'cons $x $acc}})}.
  
  
notation "x ≡ y" with precedence 45
  for @{struct_eq $x $y}.
  
notation "x ⥤ y" with precedence 45
  for @{struct_reduce $x $y}.

notation "𝐒" with precedence 45 for @{struct}.



                                                  (*            *
                                                   *  Functions *
                                                   *            *)

definition eqb_op ≝ λo1,o2.match o1 with[
  par ⇒ match o2 with [ par ⇒ true | _ ⇒ false]
| copar ⇒ match o2 with [copar ⇒ true | _ ⇒ false ]
| seq ⇒ match o2 with [seq ⇒ true | _ ⇒ false]].
 
  
let rec size_struct b ≝
  match b with [
   unit ⇒ 1
  | atom i ⇒ 1
  |  lista op l ⇒  (\fold[plus,1]_{i∈l} (size_struct i))].
  
  

                                       (*Induction on Struct*)
                                       
theorem elim_struct : ∀P : 𝐒 → Prop.  (*Made by Asperti*)
    P unit → 
    (∀t:lit. P (atom t)) →
    (∀O. P (lista O [ ])) → 
    (∀O.∀H.∀TL. P H → P ( lista O TL) → P (lista O (H::TL)) )→ 
    (∀S. P S)  .
    
  #P #U #HB #HN #HL #s
  cut (∃n. size_struct s =n)
  [% {(size_struct s)} //] (*La dimensione esiste sempre*)
  
  * as X #n lapply s -s @(nat_elim1 n) (*Induzione sulla dimensione*)
  -n #m #H #s cases s
  [ #T // | #l // (*Caso base*) 
  | (* Se s è una struttura con lista *)
    #O #l 
     cases l (*Induzione sulla lista interna *)
      [ (*Lista vuota*)
        #H1 // 
       | (*Lista con almeno un eleme  nto *)
         #st #l1
          #H1
          @HL 
           [ (*Head*)
              @(H … (refl  …)) (*La dimenione della head è minore del totale?*)
              <H1 >(plus_n_O (size_struct st)) in ⊢ (?%?); whd
              >(plus_n_Sm (size_struct st) 0) in ⊢ (?%?); @monotonic_le_plus_r
              elim l1 (*Induzione sulla coda*) // #a #tl normalize /2/ 
           | (*Tail*)
              normalize in H1; lapply(sym_eq nat …H1)  >commutative_plus -H1 #H1 lapply (eq_plus_to_le … H1)-H1 
              elim l1 (*Induzione sulla coda*)
              // (*Coda vuota*)
              #b2 #l2 #Hind normalize #H1 @HL
              [ (*Spezzo la lista, Head*)
                @(H … (refl …)) @(lt_to_le_to_lt … H1) >(plus_n_O (size_struct b2)) in ⊢ (?%?); whd
               >(plus_n_Sm (size_struct b2) 0) in ⊢ (?%?); @monotonic_le_plus_r
               elim l2 // #a #tl normalize /2/
               |
              @Hind /2/
             ]] ]]             
qed.

                                (*Syntax Equivalence*)


inductive struct_eq : 𝐒→ 𝐒 → Prop ≝ 
 | eqRif : ∀S1: 𝐒 .                  S1 ≡ S1
 | eqParComm : ∀L1,L2.       lista par (L1@L2) ≡ lista par (L2@L1)
 | eqCoparComm : ∀L1,L2.       lista copar (L1@L2) ≡ lista copar (L2@L1) 
 | eqAss : ∀L1,L2,L3.∀O.          lista O (L1@L2@L3) ≡ lista O (L1@((lista O L2)::L3))
  
 | eqComm : ∀S1,S2: 𝐒 .              S2 ≡ S1 → S1≡ S2
 | eqTrans : ∀S1,S2,S3: 𝐒 .          S1 ≡ S2 → S2 ≡ S3 → S1 ≡ S3 
 | eqUnitLeft : ∀O.∀L.              lista O L ≡ lista O (∘::L)
 | eqUnitRight : ∀O.∀L.              lista O L ≡ lista O (L@[∘])
 | eqSingleton : ∀O.∀S.              lista O [S] ≡ S
 | eqContext : ∀H1,H2.∀L1,L2.∀O.   H1 ≡ H2 → lista O L1 ≡ lista O L2 → lista O (H1::L1) ≡ lista O (H2::L2).
 
                           (*S.E Lemmas*)
 
lemma listContext : ∀L1,L2,L3.∀O.  lista O L2 ≡ lista O L3 → lista O (L1@L2) ≡ lista O (L1@L3).
  #L1 #L2 #L3 #O #h
  elim L1
    normalize //
    #H #TL #i @eqContext // qed.

lemma eqParComm2 : ∀L1,L2,L3,L4,L5.       lista par (L1@L2@L3@L4@L5) ≡ lista par (L1@L4@L3@L2@L5).
  #L1 #L2 #L3 #L4 #L5


  @listContext 
  @(eqTrans ? (lista par (L5@L2@L3@L4)) ?) 
  [ 
  @(eqTrans ? (lista par ((L2@L3@L4)@L5) ) ?) // |
  @(eqTrans ? (lista par (L5@L4@L3@L2)) ?) //
  @listContext
  @(eqTrans ? (lista par (L2@L4@L3)) ?) //
  @listContext // qed.
  
lemma eqCoparComm2 : ∀L1,L2,L3,L4,L5.       lista copar (L1@L2@L3@L4@L5) ≡ lista copar (L1@L4@L3@L2@L5).
  #L1 #L2 #L3 #L4 #L5
  @listContext 
  @(eqTrans ? (lista copar (L5@L2@L3@L4)) ?) 
  [ 
  @(eqTrans ? (lista copar ((L2@L3@L4)@L5) ) ?) // |
  @(eqTrans ? (lista copar (L5@L4@L3@L2)) ?) //
  @listContext
  @(eqTrans ? (lista copar (L2@L4@L3)) ?) //
  @listContext // qed.
  
lemma par_swap : ∀S1,S2 . 〚S1;S2〛≡〚S2;S1〛.  #S1 #S2 @(eqParComm [S1] [S2]) qed. 
lemma copar_swap : ∀S1,S2 .❨S1;S2❩≡❨S2;S1❩.  #S1 #S2 @(eqCoparComm [S1] [S2]) qed.

lemma  eqAss2 : ∀L1,L2,L3,L4.∀O.
   L1@L2@L3=L4 → lista O L4 ≡ lista O (L1@((lista O L2)::L3)). // qed.
  
lemma eqSingletonSwap : ∀S.∀O1,O2. lista O1 [(lista O2 [S])] ≡ lista O2 [(lista O1 [S])].
  #S #O1 #O2 @eqComm
  @(eqTrans ? (lista O1 [S]) ?) //
  @(eqTrans ? (lista O2 [S]) ?) /2/ @(eqTrans ? S ?) // @eqComm // qed.

lemma nil_to_unit : ∀O. lista O [ ] ≡ ∘.
  #O
  @(eqTrans ? (lista O [∘]) ?) // qed. 


lemma eqSingletonEmpty: ∀O1, O2. lista O1 [ ] ≡ lista O2 [].
  #O1 #O2
  @(eqTrans ? ∘ ?) // @eqComm // qed.

lemma eqSingUnit1 : ∀O.∀S. lista O [S;∘] ≡ S.
  #O #S
  @(eqTrans ? (lista O [S]) ?)
  [ @eqComm @eqUnitRight | @eqSingleton] qed.

lemma eqSingUnit2 : ∀O.∀S. lista O [∘;S] ≡S.
  #O #S
  @(eqTrans ? (lista O [S]) ?)
  [ @eqComm @eqUnitLeft |@eqSingleton] qed.


 
 
                                        (* Neg*)

definition neg_op ≝ λo. match o with [
  par   ⇒ copar
| copar ⇒ par
| seq   ⇒ seq ].


let rec neg s ≝
  match s with [
      lista op l ⇒ lista (neg_op op) (map ? ? neg l) 
    | unit ⇒ unit
    | atom i ⇒ match i with [ int b n ⇒ (atom (int (¬b) n)) ]
    ].
  
theorem app_neg : ∀S1,S2. S1 ≡ S2 → neg S1 ≡ neg S2.
  #S1 #S2 #H
  elim H
  /2/
  [
    #L1 #L2 normalize // |
    #L1 #L2 normalize // | |
    #O #L cases O normalize <(map_append ? ? neg L [∘]) normalize //
  ]
  #L1 #L2 #L3 #O
  cases O
  normalize
     [ letin op ≝ copar letin nop ≝ par |letin op ≝ par letin nop ≝ copar  | letin op ≝ seq letin nop ≝ seq] 
     <(map_append ? ? neg L1 ((lista nop L2)::L3)) normalize
     [ letin op ≝ copar |letin op ≝ par | letin op ≝ seq] 
     <(map_append ? ? neg L1 (L2@L3))
     @(listContext (map ? ? neg L1) (map ? ? neg (L2@L3)) ((lista op (map ? ? neg L2)::(map ? ? neg L3))) op) 
     @(eqTrans ? (lista op ((map ? ? neg L2)@(map ? ? neg L3))) ?) //
     @(eqAss ([ ]) (map ? ? neg L2) (map ? ? neg L3) op) 
qed.


             
             
             (* ∀s. neg (neg s) = s *)
              
lemma negbase : ∀t.neg (neg (atom t) )= (atom t).
  #T elim T #I elim I #B // qed.
   
lemma neglista : ∀O.∀H.∀TL. 
  ((neg (neg H))=H) → 
  (neg (neg (lista O TL))=lista O TL) → 
  (neg (neg (lista O (H::TL))) = lista O (H::TL)).
  #O #H #TL
  #H1
  normalize #H2 @eq_f2 lapply H2 -H2 elim O // normalize
  #H2
  @eq_f2 //
  destruct // qed.

  
theorem negIdem : ∀s. neg (neg s) = s.
  @elim_struct //[ #O cases O // | @neglista] qed. 


theorem neg_app : ∀S1,S2. neg S1 ≡  neg S2 → S1 ≡ S2.
  #S1 #S2 #H /2/ qed.

 
                            (* Sub struct *)

inductive sub_struct : struct → struct → Prop ≝
| it : ∀S. sub_struct S S
| inner : ∀S,S1,O,l. sub_struct S S1 → mem ? S1 l → sub_struct S (lista O l).

lemma sub_atom: ∀S,n. sub_struct S (atom n) → S = (atom n).
#S #n #Hsub inversion Hsub // #S1 #S2 #S3 #l #_ #_ #_ #_ #H destruct
qed.

lemma sub_unit : ∀S. sub_struct S (∘) → S=∘.
#S #Hsub inversion Hsub // #S1 #S2 #O #l #_ #_ #_ #_ #e destruct qed. 

lemma sub_list_atom: ∀n,O,l.  sub_struct (atom n) (lista O l) → 
  ∃S. mem ? S l ∧ sub_struct (atom n) S.
#n #O #l #Hsub inversion Hsub 
  [#S #Heq <Heq #Habs destruct
  |#S #S1 #Op #l1 #Hsub #Hmem #_ #_ #Heq destruct (Heq) %{S1} % // 
  ] qed.
  
lemma sub_list_unit : ∀O,L. sub_struct ∘ (lista O L) →  
  ∃S. mem ? S L ∧ sub_struct ∘ S.
#n #O #Hsub inversion Hsub 
  [#S #Heq <Heq #Habs destruct
  |#S #S1 #Op #l1 #Hsub #Hmem #_ #_ #Heq destruct (Heq) %{S1} % // 
  ] qed.  
  
  (*These should be in list.ma*)
lemma mem_append_l1 : ∀A.∀l1,l2:list A.∀a. (mem A a l1 ∨ mem A a l2) → mem A a (l1@l2).
#A #l1 #l2 #a #h
cases h elim l1
  [1,2: 
     normalize [ * |
        #H #TL #HI #H2 
        cases H2 -H2
          [ #x %1 // | #x %2 @HI @x]
        ]
    |3,4: normalize //
      #H #TL #Hi #h %2 @Hi //] qed.
      
      
lemma mem_append : ∀A,x,l1,l2. mem A x (l1@l2) → 
  mem A x l1 ∨ mem A x l2.
#A #x #l1 elim l1 normalize [/2/]
#a #tl #Hind #l2 * [#eqxa %1 /2/ |#memx cases (Hind … memx) /3/]
qed.


lemma sub_head_atom1 : ∀H.∀TL.∀O.∀N. sub_struct (atom N) (lista O (H::TL)) → 
    sub_struct (atom N) H ∨ sub_struct (atom N) (lista O TL).
    #H #TL #O #N #H
    lapply (sub_list_atom ? ? ? H) -H * #x * #h1 #h2
    normalize in h1;
    cases h1
    [ #hx destruct %1 // | #htl -h1 %2 @(inner (atom N) x O TL) // ] qed.
    
lemma sub_head_atom2 : ∀H.∀TL.∀O.∀N. 
    sub_struct (atom N) H ∨ sub_struct (atom N) (lista O TL) → 
    sub_struct (atom N) (lista O (H::TL)).
    #H #TL #O #N *
    [ #h @(inner (atom N) H O (H::TL)) // normalize % // |
      #h lapply (sub_list_atom ? ? ? h) * #x * #e1 #e2
      @(inner (atom N) x O (H::TL)) //
      normalize %2 // qed.
  
lemma sub1 : ∀S,S1.S≡S1 → ∀n.sub_struct (atom n) S \liff   sub_struct (atom n) S1.
(*Made by Asperti*)
#S #S1 #H elim H
  /2/
  [1,2: #L1 #L2 #n %
    #e1  cases (sub_list_atom …e1) #Sx * #Hmem #Hsub 
         cases (mem_append ???? Hmem) -Hmem #Hmem
         [1,3,5,7: @(inner … Hsub) @(mem_append_l1 ? ? ? ??) %2 // |2,4,6,8:
           @(inner … Hsub) @(mem_append_l1 ? ? ? ??) %1 //]
  | #L1 #L2   #L3 #O #n %  
    [#e1 cases (sub_list_atom …e1) #Sx * #Hmem #Hsub
     cases (mem_append ???? Hmem) -Hmem
      [#Hmem1 @(inner … Hsub) @mem_append_l1 % //
      |#Hmem2 cases (mem_append ???? Hmem2) -Hmem2
        [#Hmem2 @(inner ? (lista O L2)) 
          [@(inner … Hsub) // | @mem_append_l1 %2 normalize %1 //]
        |#mem3 @(inner … Hsub) @mem_append_l1 %2 normalize %2 //
        ]
      ]
    |#e1 cases (sub_list_atom …e1) #Sx * #Hmem #Hsub
     cases (mem_append ???? Hmem) -Hmem
      [#Hmem1 @(inner … Hsub) @mem_append_l1 %1 //
      |* 
        [#HSx >HSx in Hsub; -HSx #e2 cases (sub_list_atom …e2)
         #Sy * #HmemSy #HsubSy @(inner … HsubSy) 
         @mem_append_l1 %2  @mem_append_l1 %1 //
        |#mem3 @(inner … Hsub) @mem_append_l1 %2  @mem_append_l1 %2  //
        ]
      ]
    ]    
  |
  #O #L #N %
    [ #H1 
    @sub_head_atom2 %2 // | #H1 lapply (sub_head_atom1 ? ? ? ? H1) *
  [ #X lapply (sub_unit ? X) #f destruct | #f //] ]
  | #O #L #N %
    [ #H1 cases (sub_list_atom …H1) #x * #i #j 
     @(inner …j) 
     @mem_append_l1 % // | #H cases (sub_list_atom …H)
     #x * #e1 #e2  @(inner (atom N) x O L) // 
     lapply (mem_append ???? e1) * normalize // * #e destruct 
     [ lapply (sub_unit ? e2) #x destruct | lapply e * ]]
     | #O #Sx #n % 
    [#H1 inversion H1 
      [#Sy #HSy <HSy #Habs destruct (Habs)
      |#Sy #Sz #Op #l #Hsub #Hmem #Hind #HSy #Hl destruct (Hl) 
       lapply Hmem normalize in ⊢ (%→?); * // @False_ind
      ]
    |#Hsub @(inner … Hsub) %1 //
    ] |
       #Head1 #Head2 #L1 #L2 #O #h #H1 #H2 #H3 #N  %
    
    [ #H4 
     lapply (sub_head_atom1 ? ? ? ? H4) *
     [ -H4 #i @sub_head_atom2 % inversion i
         [ #S0 #e #e2 destruct 
         lapply (H2 N) * #H6 #H7 @H6 // |
         #S0 #S2 #O2 #L #Hsub #Hmem #e #e2 #e3 destruct
         lapply (H2 N) * #H9 #H10 @H9 // ]
         | -H4 #i @sub_head_atom2 %2 lapply (H3 N) * #H12 #H13
         @H12 // ]
     | #i 
     lapply (sub_head_atom1 ? ? ? ? i) *
        [ #f @sub_head_atom2 % -i inversion f 
          [ #S0 #e1 #e2 destruct lapply (H2 N) * #H18 #H19 @H19 // |
          #S0 #S2 #O2 #L #H21 #H22 #H23 #H24 #H25 destruct lapply (H2 N)
          * #H29 #H30 @H30 //]
        | #f @sub_head_atom2 %2 lapply (H3 N) * #H32 #H33 @H33//]]] qed.
        
        
                          (* size_atom : n° of atoms*)
  
let rec size_atom S ≝ match S with [
  unit ⇒ 0
| atom X ⇒ 1
| lista O L ⇒ (\fold[plus,0]_{i∈L} (size_atom i))].


(*These follow by nat lemmas...reason of ease*)
lemma plus_l : ∀n,m,p:nat. m=p → plus n  m=plus n  p. // qed.

lemma plus_comm :∀n,m: nat . plus n m = plus m n. // qed.

lemma plus_assoc : ∀n,m,p: nat . plus n (plus m p ) = plus (plus n m) p. // qed.


lemma size_equal : ∀R,T. R≡T → size_atom R = size_atom T.
  #R #T #H
  elim H
  //
  [1,2: #L1 #L2
  normalize
  elim L1
  elim L2
  normalize //

  #Hx #TL #Hi #H2 #TL2 #H132

  lapply (Hi H2 TL2)
  -Hi #Hi
  >H132
  lapply Hi
  lapply H132
  -Hi -H132
  letin B ≝ (fold ? ? plus O (λi:𝐒.true) (λi:𝐒.size_atom i) (TL@TL2))
  #x #y 
  lapply (plus_comm (size_atom H2) (plus (size_atom Hx) B)) 
  #e >e 
  lapply (plus_assoc (size_atom Hx) (B) (size_atom H2))
  #e2
  <e2
  @(plus_l (size_atom Hx) (plus B (size_atom H2)) ? )
  -e -e2
  normalize
  elim TL
  normalize //
  | #L1 #L2 #L3 #O 
  normalize
  elim L1
  normalize
  elim L2 //
  #H #TL #x
  normalize
  lapply x
  letin B ≝ (fold ? ? plus 0 (λi:𝐒.true) (λi:𝐒.size_atom i) TL)
  letin C ≝ (fold ? ? plus 0 (λi:𝐒.true) (λi:𝐒.size_atom i) L3)
  
    lapply (plus_assoc (size_atom H) (B) (C)) #e <e -x #x
  @(plus_l (size_atom H) ? (plus B C) ) // |
  #O #L normalize
  elim L normalize // | 
  normalize // | 
  #H1 #H2 #L1 #L2 #O #H1 #H2 #Hi #Hi2
  normalize >Hi normalize in Hi2; <Hi2 // qed.
  
lemma le_trans : ∀n,m,p . n ≤ m → m ≤ p → n ≤ p. /2/ qed.

lemma le_lr : ∀n,p,m,q . n ≤m → p ≤ q → plus n p ≤ plus m q . /2/ qed.

lemma size_neg : ∀R. size_atom (neg R) = size_atom R.
  @elim_struct // #T normalize elim T normalize // qed.
  
lemma zero_plus_zero_zero : ∀n,m. plus n m = 0 → (n=0 ∧ m=0). #n #m #h % /2/ qed.
lemma zero_zero_plus_zero : ∀n,m .n=0 ∧ m=0 → plus n m = 0. #n #m * // qed.

lemma size_zero_1 : ∀R . size_atom R =0 → R≡ ∘.
  @elim_struct
  //
  [ #T elim T normalize #b #n #a 
  lapply (sym_eq ? ? ?  a) -a #a lapply (not_eq_O_S 0)  * #A lapply (A a) * |
  #O #H #TL
  elim H
  normalize 
  [ #H39 #H40 #H41 
  lapply (H40 H41) -H40 -H41 #H1 @eqComm @(eqTrans ? (lista O TL)) /2/ | 
   #T #_ #Hi #Hi2 
  lapply (not_eq_O_S (fold ? ? plus 0 (λi:𝐒.true) (λi:𝐒.size_atom i) TL)) * #x
  lapply (sym_eq ? ? ? Hi2) -Hi2 #Hi2
  lapply (x Hi2) * | 
  #O2 #L #x #y #z 
  lapply (zero_plus_zero_zero ((fold ? ? plus 0 (λi:𝐒.true) (λi:𝐒.size_atom i) L)) (fold ? ? plus 0 (λi:𝐒.true) (λi:𝐒.size_atom i) TL) z)
  * -z #z1 #z2
  lapply (x z1) -x #x lapply (y z2) -y #y
  @(eqTrans ? (lista O (∘::TL))) [ @eqContext // | @eqComm @(eqTrans ? (lista O TL )) /2/ qed.
  
lemma size_zero_2 : ∀R . R≡ ∘ → size_atom R = 0.
  #R #h lapply (size_equal ? ? h) normalize // qed.
  
lemma size_mem : ∀L .∀O. ∀N.size_atom (lista  O L) = 0 →  mem ? (atom N) L → False.
  #L #O #N elim L normalize // #head #tail #hi #h1 * #h2
  [ destruct normalize in h1; destruct |
    @hi // lapply (zero_plus_zero_zero ? ? h1) * //] qed. 
  
lemma size_atom_mem : ∀O.∀L.∀S. mem ? S L → size_atom S ≤ size_atom (lista O L).
  #O #L #S elim L [ normalize * | #H #TL #hi #h 
  normalize cut (mem ? S ([H]@TL)) // -h #h
  lapply (mem_append ? S [H] TL h) *
  [ -h normalize * #h [ destruct @le_plus_n_r | elim h] | #i
  lapply (hi i) -hi -i #i normalize in i; @le_plus_a // qed. 

lemma size_atom_sub : ∀S1,S2. sub_struct S1 S2 → size_atom S1 ≤ size_atom S2.
  #S1 #S2 #h   elim h  //
  -S1 -S2 #S1 #S2 #O #L #H #Hi #Hi2 lapply (size_atom_mem O L S2 Hi) -Hi #Hi /2/ qed. 
        
        
                            (*S.E Lemmas*)
          
lemma unit_list_nil_false : ∀O.∀N.∀L. ∘ ≡ lista O ((atom N)::L) → False.
  #O #N #L #h  
  cut (lista O [ ] ≡ lista O ((atom N)::L)) /2/
  #_ cut ((lista O (atom N::L))≡∘) [ @eqComm //]
  -h #h lapply (size_zero_2 ? h) normalize #h destruct qed. 
    
        
lemma atom_synt_eq : ∀n,m. (atom n)≡(atom m) → (atom n)=(atom m).
  #n #m #H lapply (sub1 … H n) * #H1 #_ @sub_atom @H1 // qed.

lemma atom_unit_false : ∀n. (atom n)≡∘ → False.
  #n #h lapply (sub1 … h n) * #h1 #h2
  cut (sub_struct (atom n) ∘) [ @h1 // | #e lapply (sub_unit ? e) #f destruct ]qed.


lemma atom_nil_false : ∀O.∀N.∀L. lista O [ ] ≡ lista O ((atom N)::L) → False.
   #O #N #L #e lapply (sub1 (lista O [ ]) (lista O (atom N::L)) e N)
   *  #e1 #e2 -e -e1 cut (sub_struct (atom N) (lista O [ ]))
   [ @e2 @(inner (atom N) (atom N) O ((atom N)::L)) // normalize /2/ |
   -e2 #e inversion e 
   [ #S #a #x destruct | #S #S1 #O2 #L #a1 #a2 #x #y #z destruct
   normalize in a2; // qed.
       
                                        (*Reduction*)

inductive struct_reduce : 𝐒 → 𝐒→ Prop ≝ 
| reduceEq : ∀S1,S2:𝐒.    S1 ≡ S2 → S1 ⥤ S2
| reduceTrans:  ∀S1,S2,S3: 𝐒 .          S1 ⥤ S2 → S2 ⥤ S3 → S1 ⥤ S3
| reduceA :  ∀n:nat.     ∘ ⥤ 〚n+;n^〛
| reduceS : ∀R,T,U.      ❨ 〚R;T〛;U❩ ⥤ 〚❨R;U❩;T〛
| reduceQ : ∀R,T,U,V.     ❮〚R;U〛;〚T;V〛❯ ⥤ 〚❮R;T❯;❮U;V❯〛
| reduceContext : ∀H1,H2:𝐒.∀L1,L2.∀O. 
                H1 ⥤ H2 → (lista O L1) ⥤ (lista O L2) → (lista O (H1::L1)) ⥤  (lista O (H2::L2))
                
| reduceNeg : ∀S,T. neg S ⥤ neg T → S⥤T (*Forse si può derivare, o forse no?*).

lemma reduceRif  : ∀S. S ⥤ S. /2/ qed.

                                          
                                                  (*                *
                                                   *      Lemmi     *
                                                   *  Dimostrazioni *
                                                   *                *)                                                  
                  

lemma size_increase : ∀R,T. R⥤T → size_atom R ≤ size_atom T.
  #R #T #H
  elim H -R -T
  [ #S1 #S2 #H  lapply (size_equal ? ? H)  // |
  #S1 #S2 #S3 #H1 #H2 #Hi1 #Hi2 @(le_trans (size_atom S1) (size_atom S2) (size_atom S3)) // |
  #n normalize // |
  #R #T #U normalize // |
  #R #T #U #V normalize // |
  #H1 #H2 #L1 #L2 #O #_ #_ #Hi1 #Hi2
  normalize  
  @(le_lr (size_atom H1 ) (fold ? ? plus  0 (λi:𝐒.true) (λi:𝐒.size_atom i) L1) (size_atom H2) (fold ? ? plus 0 (λi:𝐒.true) (λi:𝐒.size_atom i) L2) ) // |
  #S #T #_ #Hi <(size_neg S) <(size_neg T) // qed.

lemma unit_to_unit : ∘ ⥤ 〚∘;neg ∘〛.
  normalize @(reduceTrans ? 〚∘〛?) @reduceEq /2/ qed.

lemma unit_to_some_par_atom : ∀t. ∘ ⥤ 〚atom t;neg(atom t)〛.
  #t 
  elim t #B  #I elim B // normalize  
  @(reduceTrans ? 〚I+;I^〛 ?) //
  @reduceEq  @(eqParComm [I+] [I^]) qed.

  
lemma unit_to_s_ns_nil : ∀o. ∘ ⥤ 〚lista o [ ] ; neg (lista o [ ])〛.
  #O @reduceEq
  @eqComm 
  @(eqTrans ? 〚(lista O [ ])〛 ?)
  [ @eqContext // elim O normalize  @(eqTrans ? 〚∘〛?) /2/ ] /2/ qed.

  
lemma unit_to_s_ns_list :   ∀O.∀H.∀TL.
  ∘⥤ 〚H;neg H〛 → 
  ∘⥤ 〚lista O TL;neg (lista O TL) 〛 → 
  ∘⥤〚lista O (H::TL); neg (lista O (H::TL))〛.
  #O #H #TL #H1
  cases O  #H2 normalize (*Per casi sugli operatori*)
        [
        @(reduceTrans ? 〚(lista copar (neg H::map ? ? neg TL)); (lista par (H::TL))〛?)
        [ | @reduceEq @par_swap]]
        [1,2:
        [letin head ≝H letin tail ≝ TL letin nHead ≝ (neg H) letin nTail ≝ (map ? ? neg TL)
        | letin head ≝ (neg H) letin tail ≝(map ? ? neg TL) letin nHead ≝ H letin nTail ≝ TL ] 
        (*Ora devo creare U grazie l'associatività*)
        @(reduceTrans ? (〚(❨nHead;(lista copar (nTail))❩); (lista par (head::tail))〛) ?)
           [2,4: @reduceEq @eqComm @eqContext [1,3:  @eqContext // /2/] //]
        (*Ora posso applicare la riduzione sulla parte destra*)
        @(reduceTrans ? (❨〚nHead; (lista par (head::tail))〛; (lista copar nTail)❩) ?)
           [2,4: @reduceS]
        (*Ora devo accoppiare H e neg H*)
        @(reduceTrans ? (❨〚(nHead); head;(lista par (tail))〛; (lista copar nTail)❩) ?)
          [2,4: @reduceEq @eqContext // 
          @eqContext //
            @(eqTrans ? ((lista par (head::tail))) ?)
              [1,3: @eqComm  @(eqAss2 [head] ? ? ?) normalize // |2,4:  @eqComm @eqSingleton]]
        @(reduceTrans ? ❨〚〚nHead; head〛; (lista par tail)〛; (lista copar nTail)❩)
          [2,4:  @reduceEq @eqComm 
            @eqContext // @(eqAss (nil ?) ([nHead;head]) ) ]
        @(reduceTrans ? (❨〚∘; (lista par tail)〛; (lista copar nTail)❩))
        [2,4: @reduceContext  /2/  @reduceContext /2/ 
          @(reduceTrans ?(〚head;nHead〛)?) [2,4: @reduceEq//] @H1]
          @reduceNeg normalize
          lapply (negIdem (lista par TL)) #nTL normalize in nTL; >nTL -nTL 
          @(reduceTrans ? 〚❨(lista copar (map ? ? neg tail))❩; (lista par tail)〛 ? )
          [2,4: @reduceEq @eqContext //]
          @(reduceTrans ? 〚(lista copar (map ? ? neg tail)); (lista par tail)〛 ? )
          [2,4: @reduceEq @eqContext // @eqComm @eqSingleton]
          @(reduceTrans ? 〚(lista par tail);(lista copar (map ? ? neg tail))〛 ? ) 
          [2,4: @reduceEq @par_swap] 
          normalize in H2; [ @H2 | normalize
          lapply (negIdem (lista copar TL)) #nTL normalize  in nTL ; >nTL -nTL
          @(reduceTrans ? 〚(lista copar TL); (lista par (map ? ? neg TL))〛 ? )
          [ | @reduceEq @par_swap] @H2   ]
          |
       (*  Voglio poter applicare questa   ❮〚R;U〛;〚T;V〛❯ ⥤ 〚❮R;T❯;❮U;V❯〛*)
          (* Porto il copar sulla sinistra*)
        (*Ora devo creare R grazie l'associatività*)
        letin nHead ≝H letin nTail ≝ TL letin head ≝ (neg H) letin tail ≝ (map ? ? neg TL) 
        @(reduceTrans ? (〚(❮nHead;(lista seq (nTail))❯); (lista seq (head::tail))〛) ?)
           [| @reduceEq @eqComm @eqContext [ @eqContext // @(eqAss2 (nil ?) ? (nil ?))/2/] //]
        (*Ora devo creare U*)
        @(reduceTrans ? (〚❮nHead; (lista seq nTail)❯; ❮head;(lista seq (tail))❯〛) ?)
         [| @reduceEq @eqComm @eqContext [ @eqContext //] @eqContext // @(eqAss2 ([head]) ? ? ?) normalize //]
        (*Ora posso applicare la riduzione sulla parte destra*)
        @(reduceTrans ? (❮〚nHead;head〛;〚(lista seq nTail);(lista seq tail)〛❯) ?)
           [ |@reduceQ]
        @(reduceTrans ? (❮∘; 〚(lista seq nTail); (lista seq tail) 〛❯))        
        [ | @reduceContext /2/]
        normalize
        @(reduceTrans ? (❮∘;∘❯))
        [2: @reduceContext /2/ @reduceContext]@reduceEq @(eqTrans ? ❮∘❯ ?) /2/] qed.
        
theorem unit_to_s_ns : ∀s. ∘⥤ 〚s;neg s〛.
  @elim_struct /2/ qed.  
  
          (*Properties*)
          
lemma copar_to_par :  ∀T,U. ❨T;U❩⥤〚T;U〛.
  #T #U
  @(reduceTrans ? 〚U;T〛?)
  [ | @reduceEq @par_swap ]
  @(reduceTrans ? 〚❨∘;U❩;T〛 ?)
  [ | @reduceEq @eqContext [ @eqSingUnit2 | @eqRif]]
  @(reduceTrans ? (❨〚∘;T〛;U❩) ?)
  [ @reduceEq @eqContext [ @eqComm @eqSingUnit2 | @eqRif] | @reduceS] qed.

lemma seq_to_par: ∀R,T . ❮R;T❯ ⥤ 〚R;T〛.
  #R #T
  @(reduceTrans ? (〚❮R❯;❮T❯〛) ?)
  [ | @reduceEq @eqContext [@eqSingleton | @eqContext //]]
  @(reduceTrans ? (〚❮R;∘❯;❮∘;T❯〛) ?)
  [ | @reduceEq @eqContext /2/ @eqContext /2/]
  @(reduceTrans ? (❮〚R;∘〛;〚∘;T〛❯) ?)
  // @reduceEq  @eqContext  /2/ @eqContext /2/ qed.


lemma seq_t: ∀R,T.∀a. ❮R;T❯⥤〚❮R;a+❯;❮a^;T❯〛.
  #R #T #a
  @(reduceTrans ? (〚❮R;a+❯;❮∘;❮a^;T❯❯〛) ?)
  [ | @reduceContext /2/ @reduceContext /2/]
  @(reduceTrans ? (❮〚R; ∘〛; 〚a+; ❮a^; T❯〛❯) ?)
  [ | @reduceQ]
  @reduceContext
  [ @reduceEq /2/]
  @reduceContext /2/ 
  @(reduceTrans ? (〚❮∘;a+❯; ❮a^; T❯〛) ?)
  [ | @reduceContext /2/]
  @(reduceTrans ? 〚❮a+;∘❯;❮a^;T❯〛 ?)
  [ 
    @(reduceTrans ? ❮〚a+;a^〛; 〚∘; T〛❯ ?) //
    @(reduceTrans ? (❮∘; T❯) ?) [ @reduceEq /2/ | @reduceContext // @reduceContext  /2/   @reduceEq /2/] |
    @(reduceTrans ? 〚❮∘;a+❯;❮a^;T❯〛 ?)
    @reduceContext /2/ @(reduceTrans ? ❮a+❯ ?)  @reduceEq /2/
  ] qed.
  

lemma t3 : ∀R,T:𝐒. ∘⥤ R ∧ ∘⥤T → ∘⥤❮R;T❯. 
  #R #T * #HR #HT
  @(reduceTrans ? R ?)
  //
  @(reduceTrans ? ❮R;∘❯ ? )
  
  [ @reduceEq /2/]
  @reduceContext /2/ qed.
  
        

lemma reduce_unit : ∀S . S ⥤ ∘ → S≡∘.
  #S #H lapply (size_increase ? ? H) normalize
  #h @(size_zero_1) /2/ qed.  
